r:CRng, u:|r|. r-Prime(u)  IsPrimeIdeal(r;(u)r) 

latex

Up	rings 1
Definitions of Statement	Rng, CRng, r-Prime(u), Ideal(r){i}, IsPrimeIdeal(R;P)
Definitions	t  T, IsPrimeIdeal(R;P), x:A. B(x), x. t(x), P  Q, P & Q, P  Q, , P  Q, x f y, P  Q, r-Prime(u), Rng, CRng, {T}, x(s), t  ...$L
Lemmas	crng wf, rng car wf, or functionality wrt iff, implies functionality wrt iff, all functionality wrt iff, princ ideal mem cond, not functionality wrt iff, and functionality wrt iff, iff functionality wrt iff, rng one wf, not wf, rng times wf, ring divs wf